ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), L:(event-info(ds;da) List).
(ecl-halt(ds;da;x)(0,L))  ((last(L).2.2)  ecl-halt-type(da;x)) 

latex

Definitions

b, t  T, P  Q, x:A. B(x), Void, x:A.B(x), Top, event-info(ds;da), last(L), t.2, Valtype(da;k), left + right, Unit, Type, Knd, ecl-halt-kind(x), x:AB(x), s = t, Id, x. t(x), a:A fp B(a), ecl(ds;da), type List, #$n, A  B, a < b, False, A, {x:A| B(x)} , , , ecl-halt(ds;da;x), f(a), case b of inl(x) => s(x) | inr(y) => t(y), ecl-halt-type(da;x), True, {T}, SQType(T), , s ~ t, inl x , inr x , tt, ff, x:A  B(x), P & Q, P  Q, f(x)?z

Lemmas

subtype rel self, ma-valtype wf, false wf, ecl-halt-nil, last wf, bfalse wf, btrue wf, assert wf, Knd sq, ecl-halt wf, le wf, event-info wf, ecl wf, fpf wf, Id wf, ecl-halt-kind wf, Knd wf, unit wf, ecl-halt-kind-last